package at.tasat.parser;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.ArrayList;

import at.tasat.cnf.Clause;
import at.tasat.cnf.Cnf;

public class DimacsParser {

	public static Cnf parse(InputStream stream) throws IOException {
		BufferedReader reader = new BufferedReader(new InputStreamReader(stream));
		String header = reader.readLine();
		while(header!=null && header.startsWith("c")){
			header = reader.readLine();
		}
		String[] headerTokens = header.split(" ");
		if (headerTokens.length != 4) {
			throw new IOException("Header must contain 4 tokens");
		}

		if (!headerTokens[0].equals("p")) {
			throw new IOException("Header must start with 'p'");
		}

		if (!headerTokens[1].toLowerCase().equals("cnf")) {
			throw new IOException("Only cnf-format supported");
		}
		// int numVariables = Integer.parseInt(headerTokens[2]);
		int numClauses = Integer.parseInt(headerTokens[3]);

		int clauseId = 0;
		Clause[] clauses = new Clause[numClauses];
		String line = reader.readLine();
		while (line != null) {
			if (line.charAt(0) != 'c') {
				if (clauseId >= numClauses) {
					throw new IOException("Found more clauses than stated in the header");
				}
				clauses[clauseId] = ReadClause(line.split(" "), clauseId);
				clauseId++;
			}
			line = reader.readLine();
		}
		reader.close();
		return new Cnf(clauses);
	}

	private static Clause ReadClause(String[] literalTokens, int clauseId) {
		ArrayList<Integer> literals = new ArrayList<Integer>();
		for (String token : literalTokens) {
			String literalToken = token.trim();
			if (literalToken.length() > 0) {
				int literal = Integer.parseInt(literalToken);
				if (literal == 0) {
					break;
				}
				literals.add(Integer.parseInt(literalToken));
			}
		}
		int[] literalsArray = new int[literals.size()];
		for (int i = 0; i < literalsArray.length; i++) {
			literalsArray[i] = literals.get(i);
		}
		return new Clause(clauseId, literalsArray);
	}
}
